es:ES, ff:FIFO, is_req, is_ack:(E), awaiting, owes_ack:(IdIdId).
(ff.C r Id)
 (i, j:ff.C. @i(awaiting(i,j):) & @i(owes_ack(i,j):))
 (i:ff.C, e:E. (ff.R(i,e))  (loc(e) = i  Id))
 (e:E. Dec(is_req(e)) & Dec(is_ack(e)))
 (i, j:ff.C, e:E. Dec(ff.S(i,j,e)))
 (i, j:ff.C, e:E. (ff.S(i,j,e))  (loc(e) = i  Id))
 plus-ify{i:l}(es;ff;is_req;is_ack;awaiting;owes_ack)
 (sndr, rcvr:ff.C, e, e':E.
 [e: rcvr is_ack sndr]
  [e': rcvr is_ack sndr]
  (e < e')
  x(e,e'].[x: rcvr is_req sndr]) 

latex

Definitions	P  Q, e loc e' , e(e1,e2].P(e), P  Q, P  Q, {T}, SQType(T), A c B, x:A. B(x), A, (e <loc e'), t  T, P & Q, P  Q, , x:A. B(x), if b then t else f fi , b, ff, @i(x:T), Dec(P), False, plus-ify{i:l}(es;ff;is_req;is_ack;awaiting;owes_ack)
Lemmas	owes ack-2-tt, rcv-it wf, es-le wf, es-locl wf, equal-bnot, Id sq, es-after wf, es-when wf, es-locl-iff, es-loc-pred, inconsistent-bool-eq, decidable equal bool, change-lemma2, snd-it-loc, event system wf, FIFO wf, bool wf, es-dtype wf, fifoR wf, decidable wf, es-loc wf, Id wf, fifoS wf, plus-ify wf, fifoC wf, es-E wf, snd-it wf, es-causl wf